| Up | rings 1 |
| Definitions of Statement | IsRing(T;plus;zero;neg;times;one), Rng |
| Definitions | t  T,  x:A. B(x), IsRing(T;plus;zero;neg;times;one), IsMonoid(T;op;id), IsGroup(T;op;id;inv), True,  T,  , P & Q, Rng, P   Q, SqStable(P) |
| Lemmas | rng wf, sq stable eqfun p, sq stable bilinear, sq stable inverse, sq stable ident, sq stable assoc, rng eq wf, eqfun p wf, bilinear wf, rng one wf, rng times wf, rng minus wf, inverse wf, rng zero wf, ident wf, rng plus wf, rng car wf, assoc wf, sq stable and |
)